package ewu

import gui.Layout
import scala.collection.mutable.ArrayBuffer
import ewu._

/**
 * Die Bound-Klasse erbt von der Klasse Anweisung und ist aehnlich einer
 * Zusicherung aufgebaut. Zu einem Bound gehoert ein Bezeichner "prefix"
 * sowie ein boolscher Ausdruck "expr".
 * 
 * Ein Bound steht vor einer Schleife und muss bei jedem Schleifendruchlauf
 * echt abnhehmen.
 */

case class Bound (prefix: String, expr: Expression) extends Anweisung {

  override def numerate(num: List[Int]) = null
  
  override def tabbate(i: Int) = {
    tabs = i
  }

  override def propagate(assV: Anweisung, assN: Anweisung): Anweisungsfolge = null

  override def propagate(assI: Anweisung): Anweisungsfolge = null

  override def trace(env: Environment, aenv: ArrayEnvironment, tt: Layout, h: Int):
                                      (String, Boolean, Int) = ("#################", true, h+1)
  
  def traceB(env: Environment, aenv: ArrayEnvironment, tmpBnd: BigInt): (String, Boolean) = {
    var ausgabe: String = "--#BOUND"
    var bed = true
    
    if(!prefix.equals(""))
      ausgabe ++= prefix

    if(tmpBnd == null)
      ausgabe ++= ": " + expr + " | " + expr.evaluate(env).get + " => true"
    else if(expr.evaluate(env).get < 0) {
      ausgabe ++= ": " + expr + " | " + expr.evaluate(env).get + " => false"
      bed = false
    }
    else if(tmpBnd > expr.evaluate(env).get)
      ausgabe ++= ": " + expr + " | " + tmpBnd + " -> " + expr.evaluate(env).get + " => true"
    else {
      ausgabe ++= ": " + expr + " | " + tmpBnd + " -> " + expr.evaluate(env).get + " => false"
      bed = false
    }

    return (ausgabe ++ "\n", bed)
  }
  
  def getValue(env: Environment, aenv: ArrayEnvironment): BigInt = {
    return expr.evaluate(env).get
  }

  def evaluate (env: Environment): Option[BigInt] = null

  override def toString: String = {
    var ausgabe: String = "--#BOUND"
    ausgabe ++= prefix ++ ": "
    ausgabe ++= expr + "\n"
    return ausgabe
  }
  
  override def toTabString: String = {
    var ausgabe: String = HM.tabString(tabs)
    ausgabe ++= "--#BOUND"
    ausgabe ++= prefix ++ ": "
    ausgabe ++= expr + "\n"
    return ausgabe
  }

  private def tab (t: Int): String = {
    if (t > 0)
      " " + tab(t-1)
    else
      ""
  }

  def reduce: Bound = Bound(prefix, expr.reduce)
  
  def getVariables(a: ArrayBuffer[Name]) = {
    expr.getVariables(a)
  }
  
  def replaceVariable(fromVar: Name, toVar: Expression) : Unit = {
    expr.replaceVariable(fromVar, toVar)
  }
  
}


 